Nuprl Definition : qrng 11,40

qrng
== <rationals
== x,y. qeq(xy)
== x,y. q_le(xy)
== x,yx + y
== , 0
== x.-(x)
== x,yx * y
== , 1
== x,y. if qeq(y; 0) then inr   else inl qdiv(xy)  fi > 
latex



clarification:

qrng
== <rationals
== x,y. qeq(xy)
== x,y. q_le(xy)
== x,yx + y
== , 0
== x.(-1) * x
== x,yx * y
== , 1
== x,y. if qeq(y; 0) then inr   else inl qdiv(xy)  fi > 
latex


Definitionsrationals, q_le(rs), r + s, -n, r * s, <ab>, x.A(x), if b then t else f fi , qeq(rs), #$n, inr x , , inl x , qdiv(rs)
FDL editor aliasesqrng

origin